\begin{tabbing}
$\forall$\=$E$:Type, ${\it pred?}$:($E$$\rightarrow$(?$E$)), ${\it info}$:($E$$\rightarrow$((:Id $\times$ Id) + (:(:IdLnk $\times$ $E$) $\times$ Id))), $V$:(Id$\rightarrow$Id$\rightarrow$Type),\+
\\[0ex]$M$:(IdLnk$\rightarrow$Id$\rightarrow$Type), $T$:(Id$\rightarrow$Id$\rightarrow$Type), ${\it init}$:($i$:Id$\rightarrow$EState(($T$($i$)))),
\\[0ex]${\it Trans}$:(\=$i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.($V$($i$,$a$)); $l$,$t$.($M$($l$,$t$)))$\rightarrow$EState(($T$($i$)))$\rightarrow$EState\+
\\[0ex](($T$($i$)))),
\-\\[0ex]${\it Choose}$:($i$,$a$:Id$\rightarrow\mathbb{N}\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$(?($V$($i$,$a$)))), ${\it Send}$:(\=$i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase(\=$k$;\+\+
\\[0ex]$a$.($V$($i$,$a$));
\\[0ex]$l$,$t$.($M$($l$,$t$))
\\[0ex])
\-\\[0ex]$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$(Msg($M$) List)),
\-\\[0ex]${\it val}$:($e$:$E$$\rightarrow$kindcase(kind($e$); $a$.($V$(loc($e$),$a$)); $l$,$t$.($M$($l$,$t$)))), ${\it time}$:($E$$\rightarrow$rationals).
\-\\[0ex]($\forall$$e$:$E$. ($\neg$($\uparrow$first($e$))) $\Rightarrow$ (loc(pred($e$)) = loc($e$) $\in$ Id))
\\[0ex]$\Rightarrow$ SWellFounded(pred!($e$;${\it e'}$))
\\[0ex]$\Rightarrow$ (val{-}axiom($E$;$V$;$M$;${\it info}$;${\it pred?}$;${\it init}$;${\it Trans}$;${\it Choose}$;${\it Send}$;${\it val}$;${\it time}$) $\in$ prop\{i:l\})
\end{tabbing}